Гомотопическая теория типов
Гомотопическая теория типов (HoTT, от англ. homotopy type theory) — математическая теория, особый вариант теории типов, снабжённый понятиями из теории категорий, алгебраической топологии, гомологической алгебры; базируется на взаимосвязи между понятиями о гомотопическом типе пространства, высших категориях и типах в логике и языках программирования.
Унивалентные основания математики — программа построения средствами гомотопической теории типов универсального формального языка, являющегося конструктивными основаниями для современных разделов математики и обеспечивающего возможность автоматической проверки правильности доказательств на компьютере. Инициирована Владимиром Воеводским в конце 2000-х годов; толчком к более широкому интересу к унивалентным основаниям послужила написанная Воеводским библиотека формализованной математики «Foundations», ставшая к середине 2010-х годов частью библиотеки UniMath и послужившая основой для многих других библиотек ; в рамках программы большим коллективом математиков была написана книга .
Математическое доказательство в гомотопической теории типов состоит в установлении «обитаемости» необходимого типа, то есть, в построении выражения соответствующего типа. Использование систем автоматического доказательства для теории эксплуатирует идею изоморфизма Карри — Ховарда, а благодаря математическому содержанию, вложенному в теоретико-типовые понятия, на формальном языке теории удаётся выразить и проверить достаточно сложные результаты из абстрактных разделов математики, которые ранее считались не формализуемыми программными средствами.
Ключевая идея теории — аксиома унивалентности
, постулирующая равенство объектов, между которыми может быть установлена эквивалентность, то есть, в гомотопической теории типов как равные рассматриваются изоморфные, гомеоморфные, гомотопически эквивалентные структуры; эта аксиома отражает важные свойства интерпретации высшей категории, а также обеспечивает техническое упрощение формального языка.История
Идея использования интуиционистской теории типов Пера Мартин-Лёфа для формализации высших категорий восходит к работе Михая Маккаи (венг. Makkai Mihály), в которой была построена система FOLDS (англ. first-order logic with dependent sorts)[1]. Ключевым отличием унивалентных оснований от идей Маккаи является принцип, согласно которому фундаментальными объектами математики являются не высшие категории, а высшие группоиды. Поскольку высшие группоиды отвечают по соответствию Гротендика гомотопическим типам, можно сказать что математика, с точки зрения унивалентных оснований, изучает структуры на гомотопических типах. Возможность прямого использования теории типов Мартин-Лёфа для описания структур на гомотопических типах является следствием построения Воеводским унивалентной модели теории типов. Построение этой модели требовало решения многочисленных технических проблем связанных с так называемыми свойствами когерентности и хотя основные идеи унивалентных оснований были сформулированны им в 2005—2006 годы, полная унивалентная модель в категории симплициальных множеств появилась только в 2009 году. В те же годы, что и эти исследования Воеводского, велись и другие работы по изучению различных связей между теорией типов и теорией гомотопий, в частности, одним из исторически важных событий, собравшим учёных, работавших в этом направлении, стал семинар в Уппсале в ноябре 2006 года[2].
В феврале 2010 года Воеводский начал создавать библиотеку на Coq, выросшую впоследствии в совместно разрабатываемую широким кругом учёных «библиотеку унивалентных оснований» .
По инициативе Воеводского, 2012—2013 академический год в Институте перспективных исследований был объявлен «годом унивалентных оснований», в сотрудничестве с Ауди и Коканом была открыта специальная исследовательская программа и в её рамках группа из математиков и специалистов по информатике работали над развитием теории. Одним из результатов года стало совместное создание участниками шестисотстраничной книги «Гомотопическая теория типов: унивалентные основания математики», выложенной на сайте программы в свободный доступ под лицензией CC-SA; для совместной работы над книгой был создан проект на GitHub[3].
Участники программы, представленные во введении к книге[4]:
- Торстен Альтенкирх (англ. Thorsten Altenkirch)
- Бенедикт Аренс (Benedikt Ahrens)
- Стив Ауди (англ. Steve Awodey)
- Брюно Баррас (Bruno Barras)
- Андрей Бауер (словен. Andrej Bauer)
- Марк Безем (Marc Bezem)
- Ив Берто (Yves Bertot)
- Бенно ван ден Берг (Benno van den Berg)
- Владимир Воеводский
- Дэниэл Грейсон (Daniel Grayson, создатель системы компьютерной алгебры Macaulay2 )
- Андре Жуайяль (фр. André Joyal)
- Тьерри Кокан
- Дэн Ликата (Dan Licata)
- Питер Лумсдейн (Peter Lumsdaine)
- Пер Мартин-Лёф
- Ассайя Махбуби (Assia Mahboubi)
- Сергей Мелихов
- Альваро Пелайо (Alvaro Pelayo)
- Эндрю Полонский (Andrew Polonsky)
- Матье Созо (Matthieu Sozeau)
- Бас Спиттерс (Bas Spitters)
- Майкл Уоррен (Michael Warren)
- Эрик Финстер (Eric Finster)
- Ноам Цейльбергер (Noam Zeilberger)
- Майкл Шульман (англ. Michael Shulman)
- Питер Эксел (англ. Peter Aczel)
- Юго Эрбелен (Hugo Herbelin, менеджер проекта разработки Coq)
Кроме того, во введении указано, что значительный вклад внесли также шестеро студентов, а также отмечен вклад более 20-ти учёных и практиков, посетивших в течение «года унивалентых оснований» Институт высших исследований (среди которых создатель семантики λ-исчисления Дана Скотт и разработчик формализаций на Coq доказательств задачи о четырёх красках и теоремы Фейта — Томпсона Жорж Гонтье ). Книга построена из двух частей — «Основания» и «Математика», в первой части излагаются основные положения и определяется инструментарий, во второй — строятся реализации введёнными средствами теории гомотопий, теории категорий, теории множеств, вещественных чисел.
Основные положения
Теория основывается на интенсиональном варианте интуиционистской теории типов Мартин-Лёфа и использует интерпретацию типов как объектов теории гомотопий и высших категорий. Так, с этой точки зрения отношение принадлежности точки пространству [math]\displaystyle{ a \in A }[/math] рассматривается как терм соответствующего типа: [math]\displaystyle{ a: A }[/math], расслоение с базой [math]\displaystyle{ X }[/math] — как зависимый тип [math]\displaystyle{ A(x) }[/math]. При этом отпадает необходимость представлять пространства в виде множеств точек, снабжённых топологией, и представлять непрерывные отображения между пространствами — как функции сохраняющие или отражающие соответствующие поточечные свойства пространств. Гомотопическая теория типов рассматривает пространства-типы и термы этих типов (точки) как элементарные понятия, а конструкции над пространствами, такие как гомотопии и расслоения, — как зависимые типы.
В формальном построении теории типов используется тип-универсум [math]\displaystyle{ \mathcal U_0 }[/math], термы которого — все прочие неуниверсальные («малые») типы, далее строятся типы [math]\displaystyle{ \mathcal U_1, \mathcal U_2, \dots }[/math] такие, что [math]\displaystyle{ U_i: U_{i+1} }[/math], притом все термы типа [math]\displaystyle{ \mathcal U_i }[/math] также являются термами типа [math]\displaystyle{ \mathcal U_{i+1} }[/math]. Зависимые типы (семейства типов) определяются как функции [math]\displaystyle{ B: A \to \mathcal U }[/math], кообласть которых — некоторый тип-универсум.
В гомотопической теории типов существует несколько способов конструирования новых типов из уже имеющихся. Базовые примеры такого рода — [math]\displaystyle{ \boldsymbol \Pi }[/math]-типы (зависимые функциональные типы, типы-произведения) и [math]\displaystyle{ \boldsymbol \Sigma }[/math]-типы (зависимые типы-суммы). Для данного типа [math]\displaystyle{ A: \mathcal U }[/math] и семейства [math]\displaystyle{ B: A \to \mathcal U }[/math] можно построить тип [math]\displaystyle{ \boldsymbol \Pi_{x:A} B(x) }[/math], термы которого — функции, кообласть которых зависит от элемента области определения (геометрически такие функции можно представлять как сечения некоторого расслоения), а также тип [math]\displaystyle{ \boldsymbol \Sigma_{x:A}B(x) }[/math], термы которого геометрически соответствуют элементам тотального пространства расслоения.
Равенство термов одного и того же типа в гомотопической теории типов может быть либо равенством «по определению» ([math]\displaystyle{ a_1 : = a_2 }[/math]), либо пропозициональным равенством. Равенство по определению влечёт пропозициональное равенство, но не наоборот. В общем случае, пропозициональное равенство термов [math]\displaystyle{ a_1 }[/math] и [math]\displaystyle{ a_2 }[/math] типа [math]\displaystyle{ A }[/math] представляется в виде непустого типа [math]\displaystyle{ \mathsf {Id}_A (a_1,a_2) }[/math], который называют типом тождества; термы этого последнего типа — это пути вида [math]\displaystyle{ p : a_1 \rightsquigarrow a_2 }[/math] в пространстве [math]\displaystyle{ A }[/math]; тип тождества [math]\displaystyle{ \mathsf {Id}_A (a_1, a_2) }[/math], таким образом, рассматривается как пространство путей (то есть непрерывных отображений единичного отрезка [math]\displaystyle{ \mathbb I }[/math] в [math]\displaystyle{ A }[/math]) из точки [math]\displaystyle{ a_1 }[/math] в точку [math]\displaystyle{ a_2 }[/math].
Аксиома унивалентности
Интуиционистская теория типов позволяет определить понятие эквивалентности типов (для типов принадлежащих одному универсуму) и построить каноническим образом функцию из типа тождества [math]\displaystyle{ A = B }[/math] в тип эквивалентности [math]\displaystyle{ A \simeq B }[/math]:
- [math]\displaystyle{ (A = B) \to (A \simeq B) }[/math].
Аксиома унивалентности, сформулированная Воеводским, утверждает, что эта функция также является эквивалентностью:
- [math]\displaystyle{ (A = B) \simeq (A \simeq B) }[/math],
то есть, тип тождества двух данных типов эквивалентен типу эквивалентности этих типов. В случае если [math]\displaystyle{ A }[/math] и [math]\displaystyle{ B }[/math] — пропозициональные типы, аксиома имеет особенно прозрачный смысл и сводится к утверждению, который иногда называют принципом экстенсиональности Чёрча: равенство высказываний логически эквивалентно их логической эквивалентности; использование этого принципа означает, что во внимание принимаются только истинностные значения высказываний, но не их смысл. Следствием аксиомы является функциональная экстенсиональность , то есть утверждение о том, что функции, значения которых равны для всех равных значений их аргументов, равны между собой. Это свойство функций имеет важное значение в информатике.
Аксиома рассматривается некоторыми философами математики в качестве точной математической формулировки основного тезиса философии математического структурализма , которая опирается на распространённую практику математических рассуждений «с точностью до изоморфизма» или «с точностью до эквивалентности»[5].
Логика, множества, группоиды
Высказывание (mere proposition, «голое высказывание») в гомотопической теории типов определяется как тип [math]\displaystyle{ P }[/math], который либо пуст, либо содержит единственный терм [math]\displaystyle{ p }[/math]; такие типы называются пропозициональными. Если тип [math]\displaystyle{ P }[/math] пуст, то соответствующее высказывание ложно, если [math]\displaystyle{ P }[/math] содержит терм [math]\displaystyle{ p }[/math] (символически — [math]\displaystyle{ p : P }[/math]), то соответствующее высказывание [math]\displaystyle{ P }[/math] истинно, а терм [math]\displaystyle{ p }[/math] рассматривается как его доказательство. Таким образом, в теории используется интуиционистская концепция истины, согласно которой истинность высказывания понимается как возможность предъявить доказательство этого высказывания.
Фрагмент гомотопической теории типов, который ограничивается операциями с пропозициональными типами, то есть с высказываниями, можно описать как логический фрагмент (логику) этой теории. Логическая дизъюнкция [math]\displaystyle{ A\vee B }[/math] соответствует в пропозициональном фрагменте типу-сумме [math]\displaystyle{ A+B }[/math], конъюнкция [math]\displaystyle{ A\wedge B }[/math] — типу-произведению [math]\displaystyle{ A \times B }[/math], импликация [math]\displaystyle{ A\Rightarrow B }[/math] — функциональному типу [math]\displaystyle{ A\to B }[/math], отрицание [math]\displaystyle{ \lnot A }[/math] — типу [math]\displaystyle{ A\to \mathbf 0 }[/math], где [math]\displaystyle{ \mathbf 0 }[/math] — это пустой тип (нуль-тип). Логика, соответствующая таким конструкциям, является вариантом интуиционистской логики, в частности, в ней не имеют места такие утверждения, как закон двойного отрицания или исключённого третьего.
Всякий тип [math]\displaystyle{ X }[/math], который содержит два или больше различных термов [math]\displaystyle{ x, y, \dots }[/math] может быть поставлен в однозначное соответствие с пропозициональным типом, который получается в результате отождествления всех термов типа [math]\displaystyle{ X }[/math], такая операция называется пропозициональным обрезанием (propositional truncation). Это позволяет провести различие между «пропозициональным уровнем» (уровнем высказываний) теории и гомотопической иерархии «высших» непропозициональных её уровней.
За уровнем высказываний следует уровень множеств. Множество в гомотопической теории типов определяется как пространство (тип) с дискретной топологией. Эквивалентно, множество [math]\displaystyle{ A }[/math] можно описать в теории как тип, такой что для любых его термов [math]\displaystyle{ a_1, a_2 :A }[/math] тип [math]\displaystyle{ \mathsf {Id}_A (a_1,a_2) }[/math] является высказыванием, то есть либо пуст (случай когда [math]\displaystyle{ a_1 }[/math] и [math]\displaystyle{ a_2 }[/math] — это различные элементы множества [math]\displaystyle{ A }[/math]), либо содержит единственный элемент (случай, когда [math]\displaystyle{ a_1 }[/math] и [math]\displaystyle{ a_2 }[/math] — это один и тот же элемент). Вслед за уровнем множеств идёт уровень группоидов (множество точек и множество путей между каждой парой точек), и уровни [math]\displaystyle{ n }[/math]-группоидов всех порядков.
Различные интерпретации теоретико-типовых понятий
Интуиционистская теория типов | Логика | Теория множеств | Теория гомотопий |
---|---|---|---|
тип [math]\displaystyle{ A }[/math] | высказывание [math]\displaystyle{ A }[/math] | множество [math]\displaystyle{ A }[/math] | пространство [math]\displaystyle{ A }[/math] |
[math]\displaystyle{ a:A }[/math] | доказательство высказывания [math]\displaystyle{ A }[/math] | [math]\displaystyle{ a }[/math] — элемент множества [math]\displaystyle{ A }[/math] | [math]\displaystyle{ a }[/math] — точка пространства [math]\displaystyle{ A }[/math] |
зависимый тип [math]\displaystyle{ B(x) }[/math] | предикат [math]\displaystyle{ B(x) }[/math] | семейство множеств | расслоение [math]\displaystyle{ B_x }[/math] |
[math]\displaystyle{ b(x) : B(x) }[/math] | условное доказательство | семейство элементов | сечение |
[math]\displaystyle{ \mathbf 0 }[/math], [math]\displaystyle{ \mathbf 1 }[/math] | [math]\displaystyle{ \bot }[/math], [math]\displaystyle{ \top }[/math] | [math]\displaystyle{ \varnothing }[/math], [math]\displaystyle{ \{ \varnothing \} }[/math] | [math]\displaystyle{ \varnothing }[/math], [math]\displaystyle{ \ast }[/math] |
[math]\displaystyle{ A + B }[/math] | [math]\displaystyle{ A \vee B }[/math] | [math]\displaystyle{ A \uplus B }[/math] (дизъюнктное объединение) | [math]\displaystyle{ A \oplus B }[/math] (копроизведение) |
[math]\displaystyle{ A \times B }[/math] | [math]\displaystyle{ A \wedge B }[/math] | [math]\displaystyle{ A \times B }[/math] (декартово произведение) | [math]\displaystyle{ A \times B }[/math] (произведение пространств) |
[math]\displaystyle{ A\to B }[/math] | [math]\displaystyle{ A \Rightarrow B }[/math] | множество функций [math]\displaystyle{ \{ f \mid f: A \to B \} }[/math] | функциональное пространство [math]\displaystyle{ B^A }[/math] |
[math]\displaystyle{ \boldsymbol \Sigma_{x:A} B(x) }[/math] | [math]\displaystyle{ \exists_{x:A}B(x) }[/math] | [math]\displaystyle{ \biguplus_{x \in A}B(x) }[/math] (дизъюнктное объединение) | тотальное пространство |
[math]\displaystyle{ \boldsymbol \Pi_{x:A} B(x) }[/math] | [math]\displaystyle{ \forall_{x:A}B(x) }[/math] | [math]\displaystyle{ \prod_{x \in A}B(x) }[/math] (декартово произведение) | пространство сечений |
[math]\displaystyle{ \mathsf{Id}_{A} }[/math] | равенство ([math]\displaystyle{ = }[/math]) | [math]\displaystyle{ \{ (x, x) \mid x \in A \} }[/math] | пространство путей [math]\displaystyle{ A^\mathbb I }[/math] |
Библиотеки и реализации HoTT
Библиотеки HoTT — несколько проектов, ведущихся на GitHub (в том же репозитории, где и размещены исходные коды книги), в которых создаются формальные описания различных разделов математики средствами систем автоматического доказательства с использованием построений гомотопической теории типов.
В проекте Владимира Воеводского, названном «Библиотека унивалентных оснований»[6], использовано специально разработанное минимальное безопасное подмножество Coq, обеспечивающее идеологическую чистоту и надёжность построений в согласовании с теорией. Проект HoTT[7] ведётся стандартными средствами Coq, реализуется в рамках исследовательской программы Института перспективных исследований, и в целом следует книге , по состоянию на 2020 год в проекте участвуют 48 разработчиков, наиболее активные — Джейсон Гросс, Майкл Шульман, Али Каглаян и Андрей Бауэр[8]. Также ведётся параллельный проект на языке Agda[9].
Существует несколько экспериментальных систем интерактивного доказательства, целиком основанных на HoTT: Arend, RedPRL, redtt, cooltt, а в Agda версии 2.6.0 добавлен так называемый «кубический режим», позволяющий полноценно использовать гомотопические типы.
Примечания
- ↑ Makkai Mihály. First Order Logic with Dependent Sorts, with Applications to Category Theory (англ.) (1995). Дата обращения: 5 декабря 2014. Архивировано 10 октября 2015 года.
- ↑ Identity Types — Topological and Categorical Structure. Workshop, Uppsala, November 13-14, 2006 (2006). Дата обращения: 5 декабря 2013. Архивировано 18 декабря 2014 года.
- ↑ Проект Исходные коды книги «Гомотопическая теория типов: унивалентные основания математики» на сайте GitHub
- ↑ HoTT, 2013, p. iii.
- ↑ Steve Awodey. Structuralism, Invariance, and Univalence // Philosophia Mathematica . — Oxford University Press, 2014. — Т. 22, № 1. — ISSN 0031-8019. — doi:10.1093/philmat/nkt030.
- ↑ Проект «Библиотека унивалентных оснований» на сайте GitHub
- ↑ Проект Гомотопическая теория типов на сайте GitHub
- ↑ HoTT Mar 20, 2011 — Oct 02, 2020 Contributions to master, excluding merge commits.
- ↑ Проект библиотеки HoTT на языке Agda на сайте GitHub
Литература
- Homotopy Type Theory: Univalent Foundations of Mathematics. — Princeton: Institute for Advanced Study, 2013. — 603 p.
- Steve Awodey, Álvaro Pelayo, Michael A. Warren. Voevodsky’s Univalence Axiom in Homotopy Type Theory (англ.) // Notices of the AMS. — 2013. — Vol. 60, no. 9. — P. 1164—1167.
- Hannes Hummel. Will Computers Redefine the Roots of Math?. When a legendary mathematician found a mistake in his own work, he embarked on a computer-aided quest to eliminate human error. To succeed, he has to rewrite the century-old rules underlying all of mathematics (англ.). Quanta Magazine (19 мая 2015). Дата обращения: 31 декабря 2017.
- Don Monroe. A new type of mathematics? (англ.) // Communications of the ACM. — 2014. — Vol. 57, no. 2. — P. 13—15. — doi:10.1145/2557446.
- Андрей Родин. Логический и геометрический атомизм от Лейбница до Воеводского // Вопросы философии. — 2016. — № 6. — С. 134—142.
Ссылки
- cs.cmu.edu/~rwh/courses/… — материалы курса по гомотопической теории типов, читаемого Робертом Харпером в Университете Карнеги — Меллон
Для улучшения этой статьи желательно: |